


public class Unification {
	// Unifier that is updated whenever unification between 2 terms is possible
	static String theta ="";
	// whenever a variable is found, it and the corresponding term are stored in sf1 & sf2
	static String sf1="";
	static String sf2="";
	// in case where both terms are functions, the depth is tracked
	static int depth=0;
	
	//the method unify, takes two strings as an input and try to to find 
	//the most general unifier for them. If both sentences have the same  
	//length an the same predicate symbols then we can try to unify them,
	// otherwise they aren't unifyable. Before unification is done, some
	//pre-processing is done on the strings where, any extra spaces before
	//or after the string are trimmed. Then predicate symbol for example "P"
	//in test case 1, is removed. Also the opening and closing brackets
	//are removed, then the string is split to terms, as they are separated
	//by comas. Then unify2 is called with two list of terms. 
	
	public static boolean unify(String s1, String s2){
		s1.trim();
		s2.trim();
		if(s1.charAt(0)!=s2.charAt(0))
			return false;
		String temp1=s1.substring(2, s1.length()-1);
		String temp2=s2.substring(2, s2.length()-1);
		String [] terms1= temp1.split(",");
		String [] terms2= temp2.split(",");
		if (terms1.length != terms2.length)
			return false;
		for (int i = 0; i < terms2.length; i++) {
		terms1[i].trim();
		terms2[i].trim();
		}
	    return unify2(terms1,terms2);
	    }
	//unify2 takes two list of terms as an input, and try to get the 
	//most general unifier for them. both lists are traversed from left
	// to right, every two corresponding terms are checked. In the first
	//two cases if any of the terms is a variable, then it goes to the 
	//corresponding term. This unifier is added to theta which is the 
	//general unifier. The third case is where both terms are atomic 
	//sentences in this case, we try to unify those two strings by 
	//calling unify on them. In case they are nested predicates, only
	// in the depth zero, the unifier would be added to the theta.
	public static boolean unify2(String [] terms1, String [] terms2){
		
		boolean flag=true;
		
		for(int i=0; i<terms1.length;i++)
		{
			if(!terms1[i].equals(terms2[i]))
			{	flag=false;
			    
				if(terms1[i].length()==1 && ((int)terms1[i].charAt(0))>=97 && ((int)terms1[i].charAt(0))<=122)
					{
		 				theta= theta+"(" +terms1[i] + "/" + terms2[i] + "),";
						sf1=terms1[i]; sf2=terms2[i];
						return  unify2(subst(terms1, terms1[i], terms2[i]),
									  subst(terms2, terms1[i], terms2[i])); 
					}
				else if(terms2[i].length()==1 && ((int)terms2[i].charAt(0))>=97 && ((int)terms2[i].charAt(0))<=122)
					{
					    theta= theta+"(" +terms2[i] + "/" + terms1[i] + "),";
						sf1=terms1[i]; sf2=terms2[i];
						return unify2(subst(terms1, terms2[i], terms1[i]),
								     subst(terms2, terms2[i], terms1[i])); 
					}
				else if (terms1[i].length()>1 && terms2[i].length()>1) 
					{ 
					  depth++;
					  boolean tempFlag= unify(terms1[i],terms2[i]);
			depth--;
					  
					  
					  if(tempFlag && depth==0)
					 { 
						  terms1[i]=sf1;terms2[i]=sf2;
						  return unify2(terms1,terms2);
					 }
					  else return false;
					}
			}
		}
		
		if (flag)
			return true;
		else 
		return false;	

	}
	
	//this method takes a list of terms, string1 and string2 as an input. 
	// The list is converted to a string, in that string whenevr string1
	//ocurs it is changed to string2
	private static String [] subst(String[] terms, String s1, String s2) {
		String temp="";
		for (int i=0; i<terms.length; i++)
				temp = temp+ terms[i]+",";
		temp=temp.replaceAll(s1, s2);
		temp=temp.substring(0,temp.length()-1);
		terms = temp.split(",");
		return terms;
		}
	
}
